\begin{tabbing}
atoms{-}distinct(${\it tab}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$i$:\{0..$\parallel$${\it tab}$$\parallel$ $^{-}$\}, $j$:\{0..$\parallel$${\it tab}$$\parallel$ $^{-}$\}.\+
\\[0ex](st{-}atom(${\it tab}$;$i$) = st{-}atom(${\it tab}$;$j$) $\in$ Atom1) $\Rightarrow$ ($i$ = $j$ $\in$ $\mathbb{Z}$)
\-
\end{tabbing}